Example 1 in [Gramlich & Lucas - PPDP'02]

Summary: Ex1a_GL02a

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (non-terminating)
• Positive results:
  1. Modular decomposition + Polynomials (MuTerm)
  2. CSRPO
  3. CSDP

CS-TRS Ex1_GL02a (file Ex1_GL02a.csr)

Functions:  eq 0 true s false inf cons take nil length

Constructors:  0 true s false cons nil

Variables:  X Y L

Arities: 

ar(eq) = 2
ar(0) = 0
ar(true) = 0
ar(s) = 1
ar(false) = 0
ar(inf) = 1
ar(cons) = 2
ar(take) = 2
ar(nil) = 0
ar(length) = 1

Replacement map: 

µ(eq)={}
µ(0)={}
µ(true)={}
µ(s)={}
µ(false)={}
µ(inf)={1}
µ(cons)={}
µ(take)={1,2}
µ(nil)={}
µ(length)={1}

Rules:  (file Ex1_GL02a)    

eq(0,0) -> true
eq(s(X),s(Y)) -> eq(X,Y)
eq(X,Y) -> false
inf(X) -> cons(X,inf(s(X)))
take(0,X) -> nil
take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
length(nil) -> 0
length(cons(X,L)) -> s(length(L))

The CS-TRS in OBJ format (file Ex1_GL02a.obj):

obj Ex1_GL02a is
  sort S .
  op eq : S S -> S [strat (0)] .
  op 0 : -> S .
  op true : -> S .
  op s : S -> S [strat (0)] .
  op false : -> S .
  op inf : S -> S .
  op cons : S S -> S [strat (0)] .
  op take : S S -> S .
  op nil : -> S .
  op length : S -> S .
  vars X Y L : S .
  eq eq(0,0) = true .
  eq eq(s(X),s(Y)) = eq(X,Y) .
  eq eq(X,Y) = false .
  eq inf(X) = cons(X,inf(s(X))) .
  eq take(0,X) = nil .
  eq take(s(X),cons(Y,L)) = cons(Y,take(X,L)) .
  eq length(nil) = 0 .
  eq length(cons(X,L)) = s(length(L)) .
endo

Negative results

1. The µ-termination of Ex1_GL02a cannot be proved by using Lucas' transformation. The TRS Ex1_GL02a_L:

       eq -> true
       eq -> eq
       eq -> false
       inf(X) -> cons
       take(0,X) -> nil
       take(s,cons) -> cons
       length(nil) -> 0
       length(cons) -> s
       

   is not terminating.

Positive results

1. The µ-termination of Ex1_GL02a is proved in [GL02a, Example 9] by a modular argument:
   • The TRS Ex1a_GL02a:

        eq(0,0) -> true
        eq(s(X),s(Y)) -> eq(X,Y)
        eq(X,Y) -> false
        

     is terminating (proved with MuTerm):

        Proof of termination for CS-TRS  Ex1a_GL02a:
     
        [eq](X1,X2) = X1 + X2 + 1
        [0] = 0
        [true] = 0
        [s](X) = X + 1
        [false] = 0
        

     hence µ-terminating.
   • The CS-TRS Ex1b_GL02a:

        inf(X) -> cons(X,inf(s(X)))
        take(0,X) -> nil
        take(s(X),cons(Y,L)) -> cons(Y,take(X,L))
        length(nil) -> 0
        length(cons(X,L)) -> s(length(L))
        

     is µ-terminating. This is proved by using Lucas' transformation: the TRS Ex1b_GL02a_L:

        inf(X) -> cons
        take(0,X) -> nil
        take(s,cons) -> cons
        length(nil) -> 0
        length(cons) -> s
        

     is terminating (proved with MuTerm):

        Proof of termination for CS-TRS  Ex1b_GL02a_L:
     
        [inf](X) = X + 1
        [cons] = 0
        [s] = 0
        [take](X1,X2) = X1 + X2 + 1
        [0] = 0
        [nil] = 0
        [length](X) = X + 1
        

   • Now, since Ex1a_GL02a is non-duplicating (regarding CSR, i.e., no replacing variable in a lhs has more ocurrences in the corresponding rhs) and layer preserving (i.e., it is not collapsing nor has a rhs whose root symbol is a shared constructor symbol), by [GL02a, Theorem 10], Ex1_GL02a is mu-terminating.

     See also the automatic modular proof computed by MuTerm

2. The µ-termination of Ex1_GL02a can also be proved by using CSRPO (proof due to Albert Rubio) and automatically by MuTerm:
   • marking map:

     	   m(cons,2)= { inf,take } = W
     	   m(s,1)= { length } = V
     	   m(take',1)= { length } = V
     	   m(length',1)= { inf,take } = W 
     	   

   • precedence:

     	   eq > true,false
     	   inf> cons,inf',s
     	   take > nil,cons,take'
     	   cons> s
     	   length > 0,s,length'
     	   

   • status:

     	   st(take) = mul
     	   

3. The µ-termination of Ex1_GL02a can also be proved by using CSDP (computed by MuTerm).